COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	the proof AXIOMS:
C00006 00003	the proof COPYPF:
C00012 ENDMK
C⊗;
the proof AXIOMS:

(DECL (X Y Z X1 X2 X3 Y1 Y2 Y3 Z1 Z2 Z3) |GROUND| VARIABLE SEXP)

(DECL (A B C A1 A2 B1 B2 C1 C2) |GROUND| VARIABLE ATOM)

(DECL (TT NNIL) |GROUND| CONSTANT ATOM)

(DECL (G G1 G2 G3) |GROUND| VARIABLE)

(DECL (CAR CDR) |GROUND→GROUND| CONSTANT)

(DECL (CONS) |GROUND⊗GROUND→GROUND| CONSTANT)

(DECL (PHI) |GROUND→TRUTHVAL| VARIABLE)

(AXIOM |∀G.ATOM(G)⊃SEXP(G)|)
8. ∀G.ATOM(G)⊃SEXP(G)
   ctxt: (1 2 4)   deps: NIL

(AXIOM |∀X Y.SEXP(CONS(X,Y))|)
9. ∀X Y.SEXP(CONS(X,Y))
   ctxt: (1 6)   deps: NIL

(AXIOM |∀G.SEXP(G)⊃ATOM(G)∨(∃X Y.G=CONS(X,Y))|)
10. ∀G.SEXP(G)⊃ATOM(G)∨(∃X Y.G=CONS(X,Y))
    ctxt: (1 2 4 6)   deps: NIL

(AXIOM |∀X Y.¬ATOM(CONS(X,Y))|)
11. ∀X Y.¬ATOM(CONS(X,Y))
    ctxt: (1 2 6)   deps: NIL

(AXIOM |∀X Y.CAR(CONS(X,Y))=X|)
12. ∀X Y.CAR(CONS(X,Y))=X
    ctxt: (1 5 6)   deps: NIL

(AXIOM |∀X Y.CDR(CONS(X,Y))=Y|)
13. ∀X Y.CDR(CONS(X,Y))=Y
    ctxt: (1 5 6)   deps: NIL

(AXIOM |∀PHI.∀A.PHI(A)∧(∀X Y.(PHI(X)∧PHI(Y)⊃PHI(CONS(X,Y)))⊃(∀X.PHI(X)))|)
14. ∀PHI.∀A.PHI(A)∧(∀X Y.(PHI(X)∧PHI(Y)⊃PHI(CONS(X,Y)))⊃(∀X.PHI(X)))
    ctxt: (1 2 6 7)   deps: NIL

(DECL (U V W U1 U2 U3 V1 V2 V3 W1 W2 W3) |GROUND| VARIABLE LIST)

(DECL (NULL) |GROUND→TRUTHVAL|)

(AXIOM |NULL(NNIL)|)
17. NULL(NNIL)
    ctxt: (3 16)   deps: NIL

(AXIOM |∀U.NULL(U)≡U=NNIL|)
18. ∀U.NULL(U)≡U=NNIL
    ctxt: (3 15 16)   deps: NIL

(AXIOM |LIST(NNIL)|)
19. LIST(NNIL)
    ctxt: (3 15)   deps: NIL

(AXIOM |∀G.LIST(G)⊃SEXP(G)|)
20. ∀G.LIST(G)⊃SEXP(G)
    ctxt: (1 4 15)   deps: NIL

(AXIOM |∀X U.¬NULL(CONS(X,U))|)
21. ∀X U.¬NULL(CONS(X,U))
    ctxt: (1 6 15 16)   deps: NIL

(TRW |∀X U.CAR(CONS(X,U))=X| |IMP(20,12)*DER*NIL|)
22. ∀X U.CAR(CONS(X,U))=X
    ctxt: (1 5 6 15)   deps: NIL

(TRW |∀X U.CDR(CONS(X,U))=U| |IMP(20,13)*DER*NIL|)
23. ∀X U.CDR(CONS(X,U))=U
    ctxt: (1 5 6 15)   deps: NIL

(AXIOM |∀X U.LIST(CONS(X,U))|)
24. ∀X U.LIST(CONS(X,U))
    ctxt: (1 6 15)   deps: NIL

(AXIOM |∀U.¬NULL(U)⊃(∃X U1.U=CONS(X,U1))|)
25. ∀U.¬NULL(U)⊃(∃X U1.U=CONS(X,U1))
    ctxt: (1 6 15 16)   deps: NIL

(AXIOM |∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))|)
26. ∀PHI.PHI(NNIL)∧(∀X U.PHI(U)⊃PHI(CONS(X,U)))⊃(∀U.PHI(U))
    ctxt: (1 3 6 7 15)   deps: NIL


the proof COPYPF:

(DECL (COPY) |GROUND→GROUND| CONSTANT)

(AXIOM |∀U.COPY(U)=IF NULL(U) THEN NNIL ELSE CONS(CAR(U),COPY(CDR(U)))|)
2. ∀U.COPY(U)=IF NULL(U) THEN NNIL ELSE CONS(CAR(U),COPY(CDR(U)))
   ctxt: (1 AXIOMS#3 AXIOMS#5 AXIOMS#6 AXIOMS#15 AXIOMS#16)   deps: NIL

(COMMENTL - TO PROVE ∀U LIST[COPY[U]] IE COPY IS TOTAL)

(∀E PHI |λU.LIST(COPY(U))| AXIOMS#26 |NIL| AXIOMS#19 AXIOMS#24)
4. LIST(COPY(NNIL))∧(∀X U.LIST(COPY(U))⊃LIST(COPY(CONS(X,U))))⊃
    (∀U.LIST(COPY(U)))
   ctxt: (1 AXIOMS#1 AXIOMS#3 AXIOMS#6 AXIOMS#15)   deps: NIL

(COMMENTL - BASIS PROOF SHOWING EQUATION PROGRESS - IE LIST[COPY[NIL]])

(TRW |LIST(COPY(NNIL))| |&2| AXIOMS#19)
6. LIST(COPY(NNIL))=
    LIST(IF NULL(NNIL) THEN NNIL ELSE CONS(CAR(NNIL),COPY(CDR(NNIL))))
   ctxt: (1 AXIOMS#3 AXIOMS#5 AXIOMS#6 AXIOMS#15 AXIOMS#16)   deps: NIL

(TRW |LIST(COPY(NNIL))| |&2*NIL| AXIOMS#19)
7. LIST(COPY(NNIL))=
    IF NULL(NNIL) THEN LIST(NNIL) ELSE LIST(CONS(CAR(NNIL),COPY(CDR(NNIL))))
   ctxt: (1 AXIOMS#3 AXIOMS#5 AXIOMS#6 AXIOMS#15 AXIOMS#16)   deps: NIL

(TRW |LIST(COPY(NNIL))| |&2*NIL*&AXIOMS#17| AXIOMS#19)
8. LIST(COPY(NNIL))=
    IF TRUE THEN LIST(NNIL) ELSE LIST(CONS(CAR(NNIL),COPY(CDR(NNIL))))
   ctxt: (1 AXIOMS#3 AXIOMS#5 AXIOMS#6 AXIOMS#15)   deps: NIL

(TRW |LIST(COPY(NNIL))| |&2*NIL*&AXIOMS#17*&AXIOMS#19| AXIOMS#19)
9. LIST(COPY(NNIL))=IF TRUE THEN TRUE ELSE LIST(CONS(CAR(NNIL),COPY(CDR(NNIL))))
   ctxt: (1 AXIOMS#3 AXIOMS#5 AXIOMS#6 AXIOMS#15)   deps: NIL

(TRW |LIST(COPY(NNIL))| |&2*NIL*&AXIOMS#17*&AXIOMS#19*DER| AXIOMS#19)
10. LIST(COPY(NNIL))
    ctxt: (1 AXIOMS#3 AXIOMS#15)   deps: NIL

(COMMENTL - ASSUME THE INDUCTION HYPOTHESIS)

(ASSUME |∀X U.LIST(COPY(U))|)
12. ∀X U.LIST(COPY(U))
    ctxt: (1 AXIOMS#1 AXIOMS#15)   deps: (12)

(COMMENTL - PROVE THE INDUCTION IMPLICANT)

(TRW |∀X U.LIST(COPY(CONS(X,U)))|
 |&2*IMP(AXIOMS#21,AXIOMS#24,12)*NIL*&AXIOMS#22*&AXIOMS#23*DER| AXIOMS#24)
14. ∀X U.LIST(COPY(CONS(X,U)))
    ctxt: (1 AXIOMS#1 AXIOMS#6 AXIOMS#15)   deps: (12)

(TRW |∀X U.LIST(COPY(U))⊃LIST(COPY(CONS(X,U)))| |IMP(14)*NIL*DER|)
15. ∀X U.LIST(COPY(U))⊃LIST(COPY(CONS(X,U)))
    ctxt: (1 AXIOMS#1 AXIOMS#6 AXIOMS#15)   deps: (12)

(COMMENTL - FINALLY DEMONSTRATE THE PHI WHICH WAS TO BE PROVEN)

(TRW |∀U.LIST(COPY(U))| |IMP(4)*&10*&15*NIL|)
17. ∀U.LIST(COPY(U))
    ctxt: (1 AXIOMS#15)   deps: (12)

(COMMENTL - PROVE ∀U COPY[U]=U)

(∀E PHI |λU.COPY(U)=U| AXIOMS#26 |NIL| AXIOMS#19 AXIOMS#24)
19. COPY(NNIL)=NNIL∧(∀X U.COPY(U)=U⊃COPY(CONS(X,U))=CONS(X,U))⊃(∀U.COPY(U)=U)
    ctxt: (1 AXIOMS#1 AXIOMS#3 AXIOMS#6 AXIOMS#15)   deps: NIL

(COMMENTL - BASIS PROOF)

(TRW |COPY(NNIL)=NNIL| |&2*IMP(AXIOMS#17)*NIL| AXIOMS#19)
21. COPY(NNIL)=NNIL
    ctxt: (1 AXIOMS#3)   deps: NIL

(COMMENTL - ASSUME THE INDUCTION HYPOTHESIS)

(ASSUME |∀X U.COPY(U)=U|)
23. ∀X U.COPY(U)=U
    ctxt: (1 AXIOMS#1 AXIOMS#15)   deps: (23)

(COMMENTL - PROVE THE INDUCTION IMPLICANT)

(TRW |∀X U.COPY(CONS(X,U))=CONS(X,U)|
 |&2*&AXIOMS#22*&AXIOMS#23*&>23*IMP(AXIOMS#21)*NIL*DER| AXIOMS#24)
25. ∀X U.COPY(CONS(X,U))=CONS(X,U)
    ctxt: (1 AXIOMS#1 AXIOMS#6 AXIOMS#15)   deps: (23)

(TRW |∀X U.COPY(U)=U⊃COPY(CONS(X,U))=CONS(X,U)| |IMP(25)*NIL*DER| AXIOMS#24)
26. ∀X U.COPY(U)=U⊃COPY(CONS(X,U))=CONS(X,U)
    ctxt: (1 AXIOMS#1 AXIOMS#6 AXIOMS#15)   deps: (23)

(COMMENTL - FINALLY DEMONSTRATE THE PHI WHICH WAS TO BE PROVEN)

(TRW |∀U.COPY(U)=U| |IMP(19)*&21*&26*NIL|)
28. ∀U.COPY(U)=U
    ctxt: (1 AXIOMS#15)   deps: (23)